\begin{tabbing}
fifo+property(${\it es}$;${\it codes}$;${\it decodes}$;$C$;$S$;$R$;$T$;${\it Req}$;${\it Ack}$;$i$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\lambda$$e$.$\exists$$j$:$C$. ($S$($j$,$i$,$e$)) $\leftarrow\leftarrow$ $f$$--$ $\lambda$$e$.$R$($i$,$e$)\+
\\[0ex]\& (\=$\forall$$e$:\{$e$:E$\mid$ $R$($i$,$e$)\} , $j$:\{$j$:$C$$\mid$ $S$($j$,$i$,$f$($e$))\} .\+
\\[0ex]${\it decodes}$($i$,$e$,(state when $e$)) = ${\it codes}$($j$,$i$,$f$($e$),(state when $f$($e$))))
\-\\[0ex]\& (\=$\forall$$e$, ${\it e'}$:\{$e$:E$\mid$ $R$($i$,$e$)\} , $j$:$C$.\+
\\[0ex]($S$($j$,$i$,$f$($e$))) $\Rightarrow$ ($S$($j$,$i$,$f$(${\it e'}$))) $\Rightarrow$ $f$($e$) c$\leq$ $f$(${\it e'}$) $\Rightarrow$ $e$ c$\leq$ ${\it e'}$)
\-\\[0ex]\& (\=$\forall$$j$:$C$.\+
\\[0ex]$\exists$\=${\it req}$:\{$e$:E$\mid$ ${\it Ack}$($j$,$i$,$e$)\} $\rightarrow$\{$e$:E$\mid$ $S$($j$,$i$,$e$) \& ${\it Req}$($j$,$e$)\} \+
\\[0ex]($\lambda$$e$.$S$($j$,$i$,$e$) \& ${\it Req}$($j$,$e$) $\leftarrow\leftarrow$ ${\it req}$$--$ $\lambda$$e$.${\it Ack}$($j$,$i$,$e$)
\\[0ex]\& ($\forall$$a$:\{$e$:E$\mid$ ${\it Ack}$($j$,$i$,$e$)\} . $\exists$$e$:\{$e$:E$\mid$ $R$($i$,$e$)\} . ($f$($e$) = ${\it req}$($a$) \& $e$ c$\leq$ $a$))
\\[0ex]\& $e$.${\it req}$($e$) is c$<$ preserving on $e$.${\it Ack}$($j$,$i$,$e$)))
\-\-\-
\end{tabbing}